\Comment{
Concurrent errors are notably easy to introduce and difficult to find,
specially in programs that follow a shared-memory programming model.
In such model, executing threads communicate by reading and updating a
shared space in memory.  Programmers need to use some locking
mechanism (e.g., monitors or semaphores) to protect access to data,
i.e., to prevent different threads from reading or writing data
inconsistently.  The undisciplined use of locks can result in blocking
(e.g., deadlocks), lack of global progress (livelocks) and incorrect
state mutation (data races). 
}

\lstset{escapeinside={\%*}{*)}}
\subfiguretopcaptrue
\begin{figure}[t]
  \centering
  \begin{small}
    \subfigure[Fragment of \texttt{Account} subject.]{
      \lstinputlisting[language=java,
        \Comment{numbers=left,numbersep=1pt,}basicstyle=\tiny]{Account.java}
      \label{fig:example:transfer}
    }
    \subfigure[Racy scheduling.]{
      \includegraphics[scale=0.5]{../ase2011/figs/transfer}
      \label{fig:example:race}
    }
    \caption{Example of data race due to improper synchronization.}
  \end{small}
  \figtabsep{}
  \vspace{-2ex}
\end{figure}

\section{Illustrative Example}

Figure~\ref{fig:example:transfer} shows a fragment of a Java class
implementing a bank account that contains a data race.  We illustrate
how \jpf{} and later \tname{} perform to find this error.  The
class \CodeIn{Account} has one field to store the amount available in
the account and a method to transfer money between accounts.  The
method
\CodeIn{transfer} withdraws money from the target account object
(denoted by reference \CodeIn{this}) and deposits money into the
account object passed as parameter.  Note the use of modifier
\CodeIn{synchronized} in the declaration of \CodeIn{transfer}.  This
has the effect of setting the target account object (i.e.,
\CodeIn{this}) as the \emph{monitor} for the method body; hence
blocking any thread that attempts to execute code that is also
protected by this monitor.  The semantics of Java monitors is defined
elsewhere~\cite{arnold00:java}.  Unfortunately, the protection used in
this example is not sufficient to prevent race.  The figure shows a
scenario where two distinct threads make calls to method
\CodeIn{transfer} on account objects \CodeIn{acc1} and \CodeIn{acc2}.
One thread transfers money from \CodeIn{acc1} to \CodeIn{acc2} and the
other does the opposite.  To facilitate illustration we separate field
reads in another statement that reads the field and stores its value
in the thread-local variable \CodeIn{tmp}.  The problem in this
example is that each thread \emph{acquires a different monitor} to
protect its critical region.  The first thread acquires monitor
\CodeIn{acc1} and the second acquires monitor \CodeIn{acc2}.  As such
no synchronization is in effect; any interleaving is
possible\Comment{\footnote{This includes interleavings that violate
sequential consistency~\cite{manson-etal-2005}.}}.
Figure~\ref{fig:example:race} shows one particular scenario of race.
The second thread reads the values of \CodeIn{acc2.amount} first, then
the first thread executes to completion, and finally the second thread
resumes using the invalid value stored in \CodeIn{tmp}.  Let us assume
that in the beginning of execution both accounts store 100 in
the \CodeIn{amount} field.  The improper synchronization results in an
incorrect modification of \CodeIn{acc2.amount} to 97 instead of 107.
This violates the state assertion in the main method as the sum of the
account balances resulted in 190 instead of 200, as expected.

\vspace{1ex}\noindent\textbf{Java PathFinder (JPF).}  It is unlikely
that the user will find a problematic scheduling by chance with a
single run of this test (i.e., \CodeIn{Account}'s main method).
Program model checkers have been proposed to systematically explore
the space of thread interleavings to find errors like this.  Java
PathFinder (JPF) is one explicit-state model checker for Java
programs.  It implements a\Comment{n extensible} Java Virtual Machine
(VM), equipped with state storage and backtracking capabilities,
different search strategies, and listeners for monitoring and
influencing the search.  For this example, JPF explores all possible
interleavings (modulo its space reduction strategies) reachable from
\CodeIn{Account}'s main method.  It took only $\sim$1s to find the
error above.  Unfortunately, the state space reachable from the tests
of arbitrary concurrent programs can be significantly larger than this
one.  JPF took 3 minutes and 39 seconds to report the same error for a
modified version of this main method involving 7 threads (see
Figure~\ref{tab:results}).

\Comment{
It finds all warnings reported in the course of 1 minute
in the first 5 seconds (see Table~\ref{table:results}). \tname{} uses
the monitoring infra-structure of JPF to compute the warnings.}

%% JavaPathfinder v6.0 - (C) RIACS/NASA Ames Research Center
%% Elapsed Time 5 seconds
\begin{figure}[t] 
\begin{verbatim}
======== summary =======
object Account 415
  field double amount
    write [Thread-3] Account.transfer(Account.java:27) [(401)] 
    read  [Thread-4] Account.transfer(Account.java:31) [(408, 415)] 
...
======== monitors =======
object Account 401
object Account 408
object Account 415
\end{verbatim}
\caption{\label{fig:output} Warnings \tname{} reports (running on top
  of JPF).}
\figtabsep{}
\end{figure}

%% \Fix{os tres erros são reflexos do acesso desprotegido ao mesmo ponto
%%   do programa, contudo o race poderia se manifestar na combinação
%%   entre o metodo transfer e os metodos (deposite, tranfer, e
%%   withdraw).Então o rabbit indica os seguintes pares de acesso que
%%   podem causar o erro tranfer, deposite; tranfer, withdraw; tranfer,
%%   tranfer }

\vspace{1ex}\noindent\textbf{\tname{}.}  For this larger
configuration \tname{} reports the corresponding warning in less than
5 seconds.  In total, it reports 3 different but positive warnings all
of which are related to the same problem: the improper synchronization
in method \CodeIn{transfer}.  \tname{} reports conflicting accesses
made within transfer and other methods of bank account that also
access the field \CodeIn{amount}, namely \CodeIn{withdraw} and
\CodeIn{deposit}.  Figure~\ref{fig:output} shows a fragment of the
output of \tname{} for the main method from
Figure~\ref{fig:example:transfer}.\Comment{ This is a compacted
version of the output that filters the potential conflicts.}  It
indicates that there is a potential race in the access of field
\CodeIn{amount} through one instance of \CodeIn{Account}.\Comment{ Lines
  beginning with \CodeIn{read} and \CodeIn{write} correspond to field
  accesses.}  The output of \tname{} is per object and per field and
  appears in tree format to indicate which object and field one access
  is associated.  Each line in leaf position shows if the access was a
  read or write, the thread that originated the access, the method and
  line of the access, and a list of locksets.  One lockset appears
  inside parentheses; the numbers inside parentheses indicate the
  different locks~\footnote{\tname{} operates at bytecode level and
  deals with Java monitors; other locking mechanisms such
  as \CodeIn{Lock}s are treated as syntactic sugar.} used in one field
  access.  For example, the report shows that the read field access
  performed by ``Thread-4'' used 2 locks simultaneously (and only
  these two): 408 and 415.  The report indicates that two different
  threads access field \CodeIn{amount} on \CodeIn{Account} object 415
  using different locks.  A description of each lock (/monitor)
  appears in the bottom of the report.  This warning is in fact
  positive and looks similar to the error JPF reports.

\Comment{
Note the user still needs to identify and fix the
fault (either in JPF or \tname{}).}


% LocalWords:  livelocks escapeinside numbersep basicstyle acc tmp PathFinder
% LocalWords:  interleavings JPF VM locksets lockset bytecode
